\begin{tabbing}
send{-}once{-}p(${\it es}$;$T$;$A$;$a$;$l$;${\it tg}$;$f$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(subtype\_rel(es{-}vartype(${\it es}$; source($l$); $x$); $A$)\+
\\[0ex]$\wedge$ \=($\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex](es{-}kind(${\it es}$; $e$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; $e$); $T$)))
\-\\[0ex]c$\wedge$ ($\exists$\=$e$:es{-}E(${\it es}$)\+
\\[0ex]((es{-}kind(${\it es}$; $e$) = rcv($l$,${\it tg}$) $\in$ Knd)
\\[0ex]c$\wedge$ \=((es{-}val(${\it es}$; $e$) = $f$(es{-}when(${\it es}$; $x$; es{-}sender(${\it es}$; $e$))) $\in$ $T$)\+
\\[0ex]$\wedge$ (es{-}kind(${\it es}$; es{-}sender(${\it es}$; $e$)) = locl($a$) $\in$ Knd)
\\[0ex]$\wedge$ \=($\forall$${\it e'}$:es{-}E(${\it es}$). \+
\\[0ex](es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$) $\in$ Knd)
\\[0ex]$\Rightarrow$ (es{-}kind(${\it es}$; es{-}sender(${\it es}$; ${\it e'}$)) = locl($a$) $\in$ Knd)
\\[0ex]$\Rightarrow$ (${\it e'}$ = $e$ $\in$ es{-}E(${\it es}$))))))
\-\-\-\-
\end{tabbing}